Nuprl Lemma : uni_sat_wf
2,24
postcript
pdf
T
:Type,
a
:
T
,
Q
:(
T
Prop). (
a
=!
x
:
T
.
Q
(
x
))
Prop
latex
Definitions
a
=!
x
:
T
.
Q
(
x
)
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s
)
,
Prop
,
t
T
origin
T:Type, a:T, Q:(T
Prop). (a =!x:T. Q(x)) 
Prop T:Type, a:T, Q:(TProp). (a =!x:T. Q(x)) Prop x:A. B(x)
Q T